(set-logic LIA)
(declare-fun _substvar_179_ () Bool)
(declare-fun _substvar_180_ () Bool)
(declare-fun _substvar_183_ () Bool)
(declare-fun _substvar_184_ () Bool)
(declare-fun _substvar_185_ () Bool)
(declare-fun _substvar_186_ () Bool)
(declare-fun _substvar_189_ () Int)
(declare-fun _substvar_190_ () Bool)
(declare-fun _substvar_193_ () Bool)
(declare-fun _substvar_194_ () Bool)
(declare-fun _substvar_205_ () Bool)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const v10 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v19 Bool)
(declare-const i0 Int)
(declare-const i1 Int)
(declare-const i3 Int)
(declare-const i5 Int)
(declare-const i6 Int)
(assert (forall ((q0 Bool) (q1 Bool)) v0))
(assert (exists ((q2 Int)) v17))
(declare-const i8 Int)
(assert (forall ((q3 Int) (q4 Int) (q5 Int)) v12))
(assert (exists ((q6 Bool) (q7 Bool) (q8 Int) (q9 Bool) (q10 Int) (q11 Int)) (=> (= q7 q7 v18 v19 q6 v12 v16) (= q10 0))))
(assert (exists ((q12 Int) (q13 Int) (q14 Int) (q15 Bool) (q16 Int)) v6))
(declare-const v20 Bool)
(assert (exists ((q17 Bool) (q18 Int) (q19 Int) (q20 Bool)) (=> (or v19 q17 q17) false)))
(declare-const v21 Bool)
(assert (exists ((q21 Bool) (q22 Int)) (=> (= q21 q21 q21 v15 v4 q21) false)))
(declare-const i9 Int)
(assert (forall ((q23 Bool) (q24 Int) (q25 Int) (q26 Bool) (q27 Bool) (q28 Int)) (=> (xor v0 q27 v6) (<= q25 q28))))
(declare-const v22 Bool)
(declare-const v23 Bool)
(declare-const v24 Bool)
(declare-const v25 Bool)
(declare-const i10 Int)
(declare-const v26 Bool)
(assert (exists ((q29 Bool) (q30 Int)) (=> (> i0 q30) _substvar_179_)))
(declare-const v27 Bool)
(declare-const v28 Bool)
(declare-const i11 Int)
(declare-const i12 Int)
(assert (forall ((q31 Int)) v5))
(check-sat)
